00100	(DE CHOICE(X E1 B2 E2)(PROG(Z1 Z2)
00110	(SETQ Z1(CAR X))(SETQ Z2(CDR X))
00120	(COND((NOT(EQ Z2 E2))(RETURN (RPLACD X(CDR Z2))))
00130	     ((EQ Z1 E1)(RETURN NIL))
00140	(T(RETURN(PROG2(RPLACA X (CDR Z1  ))(RPLACD X(COND(ANCESTRY(CHOICE1 (CADR Z1) B2))
00150	       (T B2))))))) ))
00160	
00300	(DEFPROP TRYPRF 
00400	 (LAMBDA(U)
00500	  (PROG (END B1 Z1 Z2 R)
00550	(SETQ END(LAST CLAUSES))
00600		(COND (XX (GO TRY3)))
00700		(SETQ B2 U)
00800		(SETQ E1 (LAST CLAUSES))
00900	TRY1	(SETQ E2 (LAST B2))
01000	(SETQ B1 CLAUSES)
01100	TRY1B	(SETQ XX (CONS B1 B2))
01200	TRY3
01300	(SETQ XX (CHOICE XX E1 B2 E2))
01400	(COND((NULL XX)(GO TRY7)))
01500		(SETQ Z1 (CAAR XX))
01600		(SETQ Z2 (CADR XX))
01700		(COND ((OR (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
01900		(COND ((NOT STRATEGY) (GO TRY1A)))
02000		(COND ((OR (STRATEGY Z1) (STRATEGY Z2)) (GO TRY1A)) (T (GO TRY8)))
02100	   TRY1A
02200		(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
02300		(SETQ R (RESOLVE Z1 Z2))
02500		(COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
02600		(SETQ END  (FINI CLAUSES R Z1 Z2 END))
02800	   TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
02900		(SETQ R (PARMOD Z1 Z2))
03000		(COND ((NULL R) (GO TRY8)))
03100		(SETQ END  (FINI CLAUSES R Z1 Z2 END))
03400	   TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
03500		(GO TRY3)
03600	   TRY7 (PRINT (QUOTE COUNT))
03700		(PRINT COUNT)
03800		(PRINT (QUOTE LEVEL))
03900		(PRINT LVL)
04000		(SETQ LVL (ADD1 LVL))
04100		(PRINT (QUOTE ELAPSED-TIME))
04200		(PRINT (TIMEIT))
04300		(SETQ E1 (CDR E1))
04400	(COND(ANCESTRY(COND(E1(SETQ B1 E1)(SETQ E1 END)(GO TRY1B))
04450	                   (T(GO TRY7A)))))
04500		(SETQ B2 (CDR E2))
04550	(SETQ E1 END)
04600		(COND (E2 (GO TRY1)))
04700	TRY7A	(PRINT (QUOTE NO-PROOF-FOUND))
04800		(COND (AUTO (ERR (QUOTE NOPROOF))))
04900		(UPDATE CLAUSES)
05000		(ERR (QUOTE NOPROOF))
05100	   TRY6H)) 
05200	EXPR)